Inference at * 
Iof proof for Lemma decidable implies better:


  P:, Q:(x:P.). Dec(P)  (P  Dec(Q))  Dec(P  Q) 

latex

 by Repeat (D 0 THENA Complete Auto)  

latex

 1: 

 1: 1. P : 
 1: 2. Q : x:P.
 1: 3. Dec(P)
 1:   (P  Dec(Q))  Dec(P  Q)
 .

Definitions	P  Q, Dec(P), x:A. B(x), , t  T
Lemmas	decidable wf